Solve exercise 3.15 and 3.17 #1678
Conversation
HyunggyuJang
requested review from
jdchristensen
and removed request for
mikeshulman
contrib/HoTTBookExercises.v
Outdated
| @@ -940,6 +940,7 @@ End Book_3_14. | |||
| (** Exercise 3.15 *) | |||
|
|
|||
| Section Book_3_15. | |||
| (* Propositional resizing is (implicitly) used for [forall P : HProp, (A -> P) -> P] to be on the same universe as [A] *) | |||
There was a problem hiding this comment.
"on" should be "in", and the comment should end in a period.
@mikeshulman Do you think this comment is sufficient, or should the exercise explicitly use universes and propositional resizing? (I said a bit more about what this would entail in another comment.)
There was a problem hiding this comment.
Got it; for now let me fix the preposition.
There was a problem hiding this comment.
I think it would be better to use universes and propresizing explicitly. But we could merge this now and potentially make that improvement later.
There was a problem hiding this comment.
In case @HyunggyuJang isn't familiar with using propositional resizing, here is one way to start the solution:
Definition Book_3_15_trunc@{u +} `{PropResizing} `{Funext} (A : Type@{u})
: Type@{u}.
Proof.
exact (resize_hprop@{_ u} (forall P : HProp@{u}, (A -> P) -> P)).
Defined.
Definition Book_3_15_ishprop `{PropResizing} `{Funext} (A : Type)
: IsHProp (Book_3_15_trunc A)
:= _.
Also note that the existing solution didn't actually state that the type is a proposition, so I added that as well. The rest will be essentially the same, but all results will need both propositional resizing and Funext.
There was a problem hiding this comment.
Thanks a lot for your detailed instruction, @jdchristensen. Yes, I'm not that familiar with propositional resizing, so let me just apply your instruction ASAP; besides that, I learned a lot from your comments, much appreciated, @jdchristensen!
There was a problem hiding this comment.
Reflected at 2b657ab
Note that, in Coq, we cannot express judgemental equality unlike the note in the text; I added a remark for it. @jdchristensen @mikeshulman Can you check whether it is appropriate?
There was a problem hiding this comment.
One way to express "judgemental equality" is to assert two terms as equal by a path and explicitly set the proof to idpath.
There was a problem hiding this comment.
@Alizter Thanks for your remark. Indeed I expressed judgemental equality with reflexivity tactic at https://github.com/HoTT/Coq-HoTT/pull/1678/files/da9b3099387a692ba7bd1c44620b869e01b5be2a..09102873e3e89f34087adaa752958132b97307b3#diff-ff4b6a1211719941834f9aec6bc57ef7b3203e603479e0ad60353086b6b0fe25R956
Think what you said and the way I expressed it are basically the same.
HyunggyuJang
requested review from
mikeshulman and
jdchristensen
and removed request for
mikeshulman and
jdchristensen
|
(Moving the discussion out of the inline comments on an out-of-date line.) With apologies to Dan who made this suggestion, I don't think this is quite what the exercise means. It doesn't say to prove that a resized version of However, I do also think you've found a mistake in the book. Even doing it the way I suggest, I think you're only going to get a typal computation rule, for essentially the same reason. And the book's propositional resizing is no stricter than the one in Coq, so it should also only have a typal computation rule. |
Thanks for your detailed remark. I’ll try to reflect your point. So basically, should encode the truncation as forall (P:Prop), (A -> P) -> P, then use propositional resizing to adjust P to be in the proper universe. Got it. |
|
Oh, sorry for the misunderstanding. I had assumed that the idea was to show that for any universe, you get a modality on that universe. Now I see what was meant. Hopefully my example of using PropResizing is still helpful. |
|
@HyunggyuJang This was a tricky task and I'm not exactly sure what the current state is, but are you interested in reviving this PR? I'm happy to help. |
No description provided.